open Boolean
open Data

sig Email {}
sig Nome {}
sig NomePacchetto {}
sig Descrizione {}

abstract sig Utente {
	nome : one Nome,
	email : one Email
}

sig Impiegato extends Utente {}

sig Cliente extends Utente {
	carrello : set Pacchetto,
	prenotazioni: set Pacchetto,
	wishlist : set WishListEntry
}
{
	// il carrello e le prenotazioni devono essere disgiunti
	#(carrello & prenotazioni) = 0
	// le prenotazioni e i carrelli devono essere pubblici
	all p : (carrello + prenotazioni) | p.pubblico = True
	// i pacchetti ai quali si riferiscono le wishlist entries devono far parte del carrello
	all ws : wishlist | some p : carrello | ws.pkt = p
}

sig Pacchetto {
	ID : one NomePacchetto,
	desc : one Descrizione,
	voloAndata: one Volo,
	voloRitorno: one Volo,
	alloggi: set Alloggio,
	escursioni: set Escursione,

	pubblico : one Bool,
	inModifica : lone Impiegato
}
{
	// no volo di ritorno prima del volo di andata
	precede[voloAndata.data, voloRitorno.data]
	// no escursioni prima di arrivare o dopo essere partiti
	// le escursioni non si devono sovrapporre
	all e :escursioni | escursioneValidaInP[e, this]
	// no prenotazioni prima di arrivare o dopo essere partiti
	all a : alloggi | precede[voloAndata.data, a.dataArrivo] && precede[a.dataPartenza, voloRitorno.data]
	// le prenotazioni non si devono sovrapporre
	all a1, a2 : alloggi | precede[a1.dataPartenza, a2.dataArrivo] || succede[a1.dataArrivo, a2.dataPartenza]

	inModifica != none => pubblico = False
}

abstract sig Prodotto{}

sig WishListEntry {
	pkt : one Pacchetto,
	// se prd e' vuoto significa che si vuole tutto il pacchetto
	prd : lone Prodotto
}
{
	// se il prodotto non e' vuoto allora deve fare parte del pacchetto
	prd != none => prodottoInPacchetto[prd,pkt]
}

sig CompagniaVolo {}

sig Volo extends Prodotto {
	compagnia : one CompagniaVolo,
	data : one Data
}

sig Alloggio extends Prodotto {
	dataArrivo : one Data,
	dataPartenza : one Data,
	prezzoPerNotte: one Int
}
{
	prezzoPerNotte >= 0
	precede[dataArrivo, dataPartenza]
}

sig Escursione extends Prodotto {
	dataInizio : one Data,
	dataFine : one Data,
	prezzo : one Int
}
{
	precede[dataInizio, dataFine]
	prezzo >= 0
}

fact {
	all u1,u2 : Utente | u1=u2 <=> u1.nome = u2.nome
	all u1,u2 : Utente | u1=u2 <=> u1.email = u2.email
	all p1,p2 : Pacchetto | p1 = p2 <=> p1.ID = p2.ID
}

pred show{
	#Cliente = 1
	#WishListEntry > 1
	#Pacchetto = 1
	#Volo = 2
	#Escursione = 3
}

pred escursioneValidaInP[e : Escursione, p : Pacchetto] {
	all esc : p.escursioni | e != esc => (precede[e.dataFine, esc.dataInizio] || succede[e.dataInizio, esc.dataFine])
	precede[p.voloAndata.data, e.dataInizio] && precede[e.dataFine, p.voloRitorno.data]
}

pred prodottoInPacchetto[p:Prodotto, pac:Pacchetto] {
	p in pac.voloAndata || p in pac.voloRitorno || p in pac.alloggi || p in pac.escursioni
}

pred iniziaModificaP[p, p': Pacchetto, i : Impiegato] {
	p.inModifica = none && p'.inModifica = i
}

pred finisciModificaP[p, p': Pacchetto, i : Impiegato] {
	p.inModifica = i && p'.inModifica = none
}

pred puoModificareP[p : Pacchetto, i : Impiegato] {
	p.inModifica = i
}

//equivalente per volo ritorno, id e descrizione
pred modificaVoloAndata[p,p' : Pacchetto, i : Impiegato, v : Volo] {
	puoModificareP[p,i] && p.voloAndata != v && p'.voloAndata = v
}

//equivalente per aggiunta e rimozione di un alloggio
pred aggiungiEscursione[p,p' : Pacchetto, i : Impiegato, e : Escursione] {
	puoModificareP[p,i] &&
	escursioneValidaInP[e, p] &&
	not e in p.escursioni &&
	p'.escursioni = p.escursioni + e
}

pred rimuoviEscursione[p,p' : Pacchetto, i : Impiegato, e : Escursione] {
	puoModificareP[p,i] &&
	e in p.escursioni &&
	p'.escursioni = p.escursioni - e
}

InizioModificaPermetteModifica: check {
	all p, p' : Pacchetto, i :Impiegato | (not puoModificareP[p, i] && iniziaModificaP[p,p', i] ) => puoModificareP[p',i]
} for 4 but 6 Int

SeUnPacchettoEInModificaNonPuoEssereModificatoDaAltri : check {
	all p,p',p'' : Pacchetto, i : Impiegato | iniziaModificaP[p,p',i] => (no i2:Impiegato | iniziaModificaP[p',p'',i2])
} for 4 but 6 Int

SeUnoIniziaModificaSoloLuiPuoFinirla: check {
	all p,p',p'': Pacchetto, i : Impiegato | iniziaModificaP[p,p',i] => (no i2:Impiegato | i2 != i && finisciModificaP[p',p'',i2])
} for 2 but 6 Int

AggiuntaERimozionoPortanoAStatoIniziale: check {
	all p,p',p'' : Pacchetto, i : Impiegato, e : Escursione |
		(aggiungiEscursione[p,p',i,e] && rimuoviEscursione[p',p'',i,e]) =>
			p.escursioni = p''.escursioni
} for 4 but 6 Int


pred aggiungiWishListEntry[c,c': Cliente, wle : WishListEntry] {
	not wle in c.wishlist &&
	c'.wishlist = c.wishlist + wle
}

pred rimuoviWishListEntry[c,c': Cliente, wle : WishListEntry] {
	wle in c.wishlist &&
	c'.wishlist = c.wishlist - wle
}

pred aggiungiPacchettoAlCarrello[c,c': Cliente, p : Pacchetto] {
	not p in c.carrello &&
	c'.carrello = c.carrello + p
}

pred rimuoviPacchettoDalCarrello[c,c': Cliente, p : Pacchetto] {
	p in c.carrello &&
	no wle : c.wishlist | wle.pkt = p &&
	c'.carrello = c.carrello - p
}

pred prenotaPacchetto[c,c': Cliente, p :Pacchetto] {
	//nota: la condizione su Cliente che obblica carrello e prenotazione ad essere disgiunte forza il fatto che
	// not p in c.prenotazioni e not p in c'.carrello
	p in c.carrello &&
	p in c'.prenotazioni
}

// sempre necessario avere 6 Int perche' e' la dimensione minima per rappresentare la data (31 necessita di 6 bits)
run show for 5 but 2 CompagniaVolo, 6 Int
run iniziaModificaP for 3 but 6 Int
run finisciModificaP for 3 but 6 Int
run modificaVoloAndata for 4 but 6 Int
run aggiungiEscursione for 4 but 6 Int, 8 Data
run rimuoviEscursione for 4 but 6 Int
run aggiungiWishListEntry for 4 but 6 Int
run rimuoviWishListEntry for 4 but 6 Int
run aggiungiPacchettoAlCarrello for 4 but 6 Int
run rimuoviPacchettoDalCarrello for 4 but 6 Int
run prenotaPacchetto for 4 but 6 Int
